$\forall$$i$:Id, $X$, $T$:Type, $x_{0}$:$X$, $P$:($X$$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal($X$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:$X$. Dec($\exists$$v$:$T$. $P$($x$,$v$)))
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.pre{-}init1{-}p(${\it es}$;$i$;"x";$X$;$x_{0}$;"a";$T$;$P$)